T:Type, as:T List, f, g:(T).
T  
 sorted(as)
 no_repeats(T;as)
 (priority-select(f;g;as) = inl(true)  +Unit
 (
 ((aas.f(a) & (b:T. (b  as)  b<a  g(b)))) 

latex

Definitions	P & Q, x:A. B(x), sorted(L), (xL.P(x)), t  T, x:A. B(x), b, A, Prop, P  Q, (x  l), x. t(x), P  Q, {i..j}, False, ||as||, i  j < k, AB, l[i], P  Q, Unit, true, priority-select(f;g;as), , S  T, no_repeats(T;l), , P  Q, Dec(P), A & B, {T}, SQType(T)
Lemmas	decidable int equal, strict-sorted, le wf, decidable lt, select member, no repeats wf, sorted wf, priority-select-property, iff functionality wrt iff, bool wf, priority-select wf, btrue wf, unit wf, int seg wf, select wf, length wf1, l exists wf, l member wf, not wf, assert wf